COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDVAR x x0 x1 x2 y y0 y1 y2 z z0 z1 z2 ε block
C00005 ENDMK
C⊗;
declare INDVAR x x0 x1 x2 y y0 y1 y2 z z0 z1 z2 ε block;
declare INDCONST A B C D E F G Table ε block;

declare INDVAR s s0 s1 s2 ε situation;
declare INDCONST S0 ε situation;

declare PREDCONST on(block,block,situation);
declare PREDCONST above(block,block,situation);
declare PREDCONST clear(block,situation);
declare PREDCONST reachable(situation) [pre];
declare PREDCONST exists(block,situation);
declare OPCONST color(block,situation) = iscolor [pre];
declare INDCONST Red Green Brown Blue ε colors;


declare OPCONST move(block,block,situation) = situation;
declare OPCONST create(block,color,situation) = situation;

axiom above:
	∀x y s.(on(x,y,s) ⊃ above(x,y,s))
	∀x s.¬above(x,x,s)
	∀x y z s.(above(x,y,s) ∧ above(y,z,s) ⊃ above(x,z,s))
;;

axiom move:
	∀x y s.(clear(x,s) ∧ (clear(y,s) ∨ y = Table) ∧ ¬(x = y) ⊃
		∀y1.(on(x,y1,move(x,y,s)) ≡ y1 = y) ∧
		∀z1 z2.(¬(z1 = x) ⊃ (on(z1,z2,move(x,y,s)) ≡ on(z1,z2,s))))
;;

axiom distinct:
	¬(A=B ∨ A=C ∨ A=D ∨ A=Table ∨ B=C ∨ B=D ∨ B=Table ∨ C=D ∨ C=Table ∨
		D=Table)
;;

axiom allblock:
	∀x.(x=A ∨ x=B ∨ x=C ∨ x=D ∨ x=Table)
;;

axiom table:
	∀x s.¬on(Table,x,s);;

axiom clear:
	∀x s.(clear(x,s) ≡ ∀y.¬on(y,x,s))
;;

axiom unique:
	∀x y1 y2 s.(on(x,y1,s) ∧ on(x,y2,s) ⊃ y1 = y2)
	∀x1 x2 y s.(¬(y=Table) ∧ on(x1,y,s) ∧ on(x2,y,s) ⊃ x1 = x2)
;;

axiom reachable:
	∀x y s.(reachable s ⊃ reachable move(x,y,s))
;;

axiom s0:
	reachable S0
	on(A,B,S0)
	on(B,C,S0)
	on(C,Table,S0)
	on(D,Table,S0)
;;

axiom colors:
	color(A,S0) = Red
	color(B,S0) = Green
	color(C,S0) = Brown
	color(D,S0) = Brown
;;

axiom s0:
	¬exists(D,S0) ∧ ¬exists(E,S0) ∧ ¬exists(F,S0) ∧ ¬exists(G,S0)
;;

axiom exists:
	∀x y s.(on(x,y,s) ⊃ exists(x,s))
;;

axiom create:
	∀s s1 x c.(¬exists(x,s) ∧ s1 = create(x,c,s) ⊃ color(x,s1) = c
∧ on(x,Table,s1))
;;